./smc.sh pnueli-zuck.5.prism pnueli-zuck.props -prop live -heuristic RTDP_ADJ -RTDP_ADJ_OPTS 1 -colourParams S:100000,Av:10,e:0.05,d:0.05,p:0.05,post:64
PRISM-games
===========
Version: 2.0.beta3
Date: Fri Mar 20 07:59:11 UTC 2020
Hostname: 68eec9c801d9
Memory limits: cudd=1g, java(heap)=8.9g
Command line: prism pnueli-zuck.5.prism pnueli-zuck.props -prop live -heuristic RTDP_ADJ -RTDP_ADJ_OPTS 1 -colourParams 'S:100000;Av:10;e:0.05;d:0.05;p:0.05;post:64' -javamaxmem 10g
Parsing the model file "pnueli-zuck.5.prism"...
Parsing properties file "pnueli-zuck.props"...
1 property:
(1) "live": Pmax=? [ F (p1=10) ]
Type: MDP
Modules: process0 process1 process2 process3 process4
Variables: p0 p1 p2 p3 p4
---------------------------------------------------------------------
Model checking: "live": Pmax=? [ F (p1=10) ]
Starting heuristic: RTDP_ADJ
IsMDP false Collapse false break false
ColourParams: S:100000 Av: 10 eps: 0.05 delta: 0.05 pmin: 0.05
TransDelta: 7.812500000000001E-10
HeuristicSG: Version try0
Grey
======================================
JSON: {"Trials":100000,"Precision":0,"PartialTransDelta":4.777556948478826E-7,"Value":{"Upper":1,"Lower":1},"ActionsOfs0":{"Action0":"[1.0;1.0]","Action1":"[1.0;1.0]","Action2":"[1.0;1.0]","Action3":"[1.0;1.0]","Action4":"[1.0;1.0]"},"GlobalTimerSecs":293.642,"AvgConf":0.8836096156191111,"StateInfos":{"num00":0,"num11":109597,"numStates":150474,"num01":40877,"avgDist":0.27165490383720775,"numWorking":0,"numUnset":0,"numClose":109597}}
Model checking completed in 294.138 secs.
Result (maximum probability): 1.0